Section: New Results

Authorization for the Social Web: from Formal Analysis to Concrete Attacks

Participants : Chetan Bansal [BITS Goa] , Karthikeyan Bhargavan [correspondant] , Sergio Maffeis [Imperial College] .

Social sign-on and social sharing are becoming an ever more popular feature of web applications. This success is caused in part by the APIs support offered by leading websites such as Facebook, Twitter and Google, and by the openness of standards such as OAuth 2.0. A formal analysis of such protocols must account for malicious websites and their JavaScript, and common website vulnerabilities, such as cross site request forgery and open redirectors.

We present a formal model for web application protocols called WebSpi, implemented as a library for the protocol verification tool ProVerif. We use WebSpi to model and verify several configurations of the OAuth 2.0 protocol. We show that our formal analysis can be used to reconstruct concrete website attacks. Our approach is validated by finding dozens of previously unknown vulnerabilities in popular websites such as Yahoo and Wordpress, when they connect to social networks such as Twitter and Facebook.

We are in discussion with Facebook, Twitter and other websites to address the vulnerabilites found by our analysis. We have submitted a paper describing this work, and plan to release the WebSpi library in 2012.